/*
 * Kodkod -- Copyright (c) 2005-present, Emina Torlak
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
 * copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be included in
 * all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
 * THE SOFTWARE.
 */
package kodkod.instance;

import java.util.Collection;
import java.util.List;

import kodkod.engine.CapacityExceededException;
import kodkod.util.ints.IntSet;
import kodkod.util.ints.Ints;

/**
 * A factory class that facilitates creation of tuples and tuple sets drawn from
 * a given universe. Only one factory per universe exists.
 *
 * @specfield universe: Universe
 * @invariant no f: TupleFactory - this | f.universe = this.universe
 * @author Emina Torlak
 */
public final class TupleFactory {

    private final Universe universe;
    private final int      base;

    /**
     * Constructs a factory for the given universe.
     *
     * @requires no (TupleFactory<:universe).universe
     * @ensures this.universe' = universe
     * @throws NullPointerException universe = null
     */
    TupleFactory(Universe universe) {
        this.universe = universe;
        this.base = universe.size();
    }

    /**
     * Returns the universe to which this factory belongs.
     *
     * @return this.universe
     */
    public Universe universe() {
        return universe;
    }

    /**
     * Returns a tuple that contains the specified sequence of atoms, drawn from
     * this.universe.
     *
     * @return {t: Tuple | t.universe = this.universe && t.atoms = atoms }
     * @throws NullPointerException atoms = null
     * @throws IllegalArgumentException atoms.length < 1
     * @throws IllegalArgumentException some a: atoms[int] | a !in
     *             this.universe.atoms[int]
     */
    public Tuple tuple(Object... atoms) {
        if (atoms.length < 1)
            throw new IllegalArgumentException("atoms.length<1");
        return new IntTuple(atoms);
    }

    /**
     * Returns a tuple that contains the specified sequence of atoms, drawn from
     * this.universe.
     *
     * @return {t: Tuple | t.universe = this.universe && t.atoms = atoms }
     * @throws NullPointerException atoms = null
     * @throws IllegalArgumentException atoms.size < 1
     * @throws IllegalArgumentException some a: atoms[int] | a !in
     *             this.universe.atoms[int]
     */
    public Tuple tuple(List< ? > atoms) {
        if (atoms.size() < 1)
            throw new IllegalArgumentException("atoms.size()<1");
        return new IntTuple(atoms.toArray());
    }

    /**
     * Returns a tuple with the specified arity whose index in an arity-dimensional
     * space over this.universe is given by the index parameter.
     *
     * @return {t: Tuple | t.universe = this.universe && t.arity = arity && index =
     *         sum({i : [0..arity) | universe.index(t.atoms[i]) *
     *         universe.size^(arity - 1 - i))}) }
     * @throws IllegalArgumentException arity < 1 || index < 0 || index >=
     *             universe.size^arity
     */
    public Tuple tuple(final int arity, final int index) {
        return new IntTuple(arity, index);
    }

    /**
     * Returns a set of all tuples of the given arity, drawn from this.universe.
     *
     * @return { s: TupleSet | s.universe = this.universe && s.arity = arity &&
     *         s.tuples = {t: Tuple | t.universe = this.universe && t.arity = arity}
     *         }
     * @throws IllegalArgumentException arity < 1
     */
    public TupleSet allOf(int arity) {
        return new TupleSet(universe, arity, 0, ((int) Math.pow(base, arity)) - 1);
    }

    /**
     * Returns a set of tuples of arity 1, each of which wraps one of the given
     * objects. The method requires that the specified object be atoms in
     * this.universe.
     *
     * @return {s: TupleSet | s.universe = this.universe && s.arity = 1 && s.tuples
     *         = { t: Tuple | t.universe=this.universe && t.arity=1 && t.atoms[0] in
     *         atoms[int]}}
     * @throws NullPointerException atoms = null
     * @throws IllegalArgumentException some atoms[int] - this.universe.atoms[int]
     */
    public TupleSet setOf(Object... atoms) {
        final TupleSet ret = new TupleSet(universe, 1);
        for (Object atom : atoms) {
            ret.add(new IntTuple(atom));
        }
        return ret;
    }

    /**
     * Returns a tuple set consisting of specified tuples. The method requires that
     * all given tuples have the same arity and be drawn from this.universe.
     *
     * @return {s: TupleSet | s.universe = this.universe && s.arity = first.arity &&
     *         s.tuples = first + rest[int] }
     * @throws NullPointerException first = null || rest = null
     * @throws IllegalArgumentException first.universe != this.universe
     * @throws IllegalArgumentException some t: rest[int] | t.universe !=
     *             this.universe || t.arity != first.arity
     */
    public TupleSet setOf(Tuple first, Tuple... rest) {
        if (!first.universe().equals(universe))
            throw new IllegalArgumentException("first.universe != this.universe");

        final TupleSet ret = new TupleSet(universe, first.arity(), first.index(), first.index());
        for (Tuple tuple : rest) {
            ret.add(tuple);
        }
        return ret;
    }

    /**
     * Returns a tuple set consisting of specified tuples. The method requires that
     * all given tuples have the same arity and be drawn from this.universe.
     *
     * @return {s: TupleSet | s.universe = this.universe && s.arity = first.arity &&
     *         s.tuples = tuples }
     * @throws NullPointerException tuples = null
     * @throws IllegalArgumentException tuples.isEmpty()
     * @throws IllegalArgumentException tuples.universe != this.universe ||
     *             #tuples.arity > 1
     */
    public TupleSet setOf(Collection<Tuple> tuples) {
        if (tuples.isEmpty())
            throw new IllegalArgumentException("tuples.isEmpty()");
        final TupleSet ret = new TupleSet(universe, tuples.iterator().next().arity());
        for (Tuple t : tuples) {
            ret.add(t);
        }
        return ret;
    }

    /**
     * Returns a set of the given arity that contains all tuples whose indeces are
     * contained in the given int set. Throws an IllegalArgumentException if the set
     * contains an index that is either negative or greater than
     * this.universe.size()^arity - 1. The returned TupleSet is backed by a clone of
     * tupleIndices.
     *
     * @requires tupleIndices is cloneable
     * @return {s: TupleSet | s.universe = this.universe && s.arity = arity &&
     *         s.tuples = {t: Tuple | t.index() in tupleIndices} }
     * @throws NullPointerException tupleIndices = null
     * @throws IllegalArgumentException tupleIndices is uncloneable
     * @throws IllegalArgumentException arity < 1
     * @throws IllegalArgumentException tupleIndices.min() < 0 || tupleIndices.max()
     *             >= this.universe.size()^arity
     */
    public TupleSet setOf(int arity, IntSet tupleIndices) {
        try {
            return new TupleSet(universe, arity, tupleIndices.clone());
        } catch (CloneNotSupportedException cne) {
            throw new IllegalArgumentException("uncloneable int set");
        }
    }

    /**
     * Returns an initially empty tuple set of the given arity, based on
     * this.universe.
     *
     * @return { s: TupleSet | s.universe = this.universe && s.arity = arity && no
     *         s.tuples }
     * @throws IllegalArgumentException arity < 1
     */
    public TupleSet noneOf(int arity) {
        return new TupleSet(universe, arity);
    }

    /**
     * Returns a tuple set that contains all tuples between <code>from</code> and
     * <code>to</code>, inclusive. More formally, the returned set contains all
     * tuples whose indices are in the range [from.index()..to.index()].
     *
     * @return { s: TupleSet | s.universe = this.universe && s.arity = from.arity &&
     *         s.tuples = {t: Tuple | t.universe = this.universe && t.arity =
     *         s.arity && from.index()<=t.index()<=to.index() }}
     * @throws NullPointerException from = null || to = null
     * @throws IllegalArgumentException from.arity != to.arity
     * @throws IllegalArgumentException from.universe != this.universe ||
     *             to.universe != this.universe
     * @throws IllegalArgumentException from.index > to.index
     */
    public TupleSet range(Tuple from, Tuple to) {
        if (from.arity() != to.arity())
            throw new IllegalArgumentException("from.arity!=to.arity");
        if (!(from.universe().equals(universe) && to.universe().equals(universe)))
            throw new IllegalArgumentException("from.universe != this.universe || to.universe != this.universe");
        return new TupleSet(universe, from.arity(), from.index(), to.index());
    }

    /**
     * Returns a tuple set that contains all tuples in the specified area of the
     * n-dimensional space, where n is the arity of the argument tuples. For
     * example, suppose that this.universe consists of atoms {atom0, atom1, atom2,
     * atom3}, where atom0 has index 0, atom1 has index 1, etc. Calling this method
     * with tuples [atom0, atom2] and [atom1, atom3] as the first and second
     * arguments would result in the set {[atom0, atom2], [atom0,atom3],
     * [atom1,atom2], [atom1, atom3]}. That is, the returned set consists of all
     * points in the rectangle whose upper left corner is the point [atom0, atom2]
     * and whose lower right corner is at [atom1, atom3].
     *
     * @return {s: TupleSet | s.arity = upperLeft.arity && s.universe =
     *         this.universe && s.tuples = {t: Tuple | all i: [0..s.arity) |
     *         this.universe.index(upperLeft.atoms[i]) <=
     *         this.universe.index(t.atoms[i]) <=
     *         this.universe.index(lowerRight.atoms[i]}}
     * @throws NullPointerException upperLeft = null || lowerRight = null
     * @throws IllegalArgumentException upperLeft.arity != lowerRight.arity
     * @throws IllegalArgumentException lowerRight.universe != this.universe ||
     *             upperLeft.universe != this.universe
     * @throws IllegalArgumentException some i: [0..upperLeft.arity) |
     *             this.universe.index(upperLeft.atoms[i]) >
     *             this.universe.index(lowerRight.atoms[i])
     */
    public TupleSet area(Tuple upperLeft, Tuple lowerRight) {
        if (!upperLeft.universe().equals(universe) || upperLeft.arity() != lowerRight.arity())
            throw new IllegalArgumentException();
        TupleSet ret = new TupleSet(universe, 1, upperLeft.atomIndex(0), lowerRight.atomIndex(0));
        for (int i = 1; i < upperLeft.arity(); i++) {
            ret = ret.product(new TupleSet(universe, 1, upperLeft.atomIndex(i), lowerRight.atomIndex(i)));
        }
        return ret;
    }

    /**
     * Throws a CapacityExceededException if all tuples of the given arity drawn
     * from this.universe cannot be represented as an integer.
     *
     * @throws CapacityExceededException if all tuples of the given arity drawn from
     *             this.universe cannot be represented as an integer.
     */
    void checkCapacity(int arity) {
        if (StrictMath.pow(base, arity) > Integer.MAX_VALUE) {
            throw new CapacityExceededException("Arity too large (" + arity + ") for a universe of size " + universe.size(), Ints.nCopies(arity, base));
        }
    }

    /**
     * Projects the tuple with the specified index and arity onto the specified
     * column.
     *
     * @requires tupleIndex >= 0 && tupleIndex < this.universe.size() ^ arity
     * @return this.universe.index(this.tuple(arity, tupleIndex).atoms[i])
     */
    int project(int tupleIndex, int arity, int column) {
        if (column < 0 || column >= arity)
            throw new IndexOutOfBoundsException(column + "");
        return (tupleIndex / ((int) Math.pow(base, arity - 1 - column))) % base;
    }

    /**
     * An implementation of the Tuple interface that stores only the tuple's arity
     * and index, rather than the full sequence of atoms. Parts of the sequence are
     * computed on demand, e.g. when the <code>get</code> method is invoked.
     *
     * @specfield universe: TupleFactory.this.universe
     * @specfield arity: int
     * @specfield index: int
     * @invariant arity >= 1 && 0 <= index < TupleFactory.this.base^arity
     * @invariant index = sum({i: [0..arity) |
     *            TupleFactory.this.universe.index(atoms[i]) *
     *            TupleFactory.this.base^(arity - 1 - i))
     * @author Emina Torlak
     */
    private final class IntTuple extends Tuple {

        private final int arity, index;

        /**
         * Constructs a tuple with the specified arity and index, whose atoms are drawn
         * from the factory's universe.
         *
         * @ensures this.arity' = arity && this.index' = index
         * @throws IllegalArgumentException arity < 1 || index < 0 || index >=
         *             TupleFactory.this.base^arity
         */
        IntTuple(final int arity, final int index) {
            checkCapacity(arity);
            if (arity < 1 || index < 0 || index >= Math.pow(base, arity)) {
                throw new IllegalArgumentException("arity < 1 || index < 0 || index >= universe.size^arity");
            }
            this.arity = arity;
            this.index = index;
        }

        /**
         * Constructs a tuple that contains the specified sequence of atoms, drawn from
         * the enclosing factory's universe.
         *
         * @requires atoms.length > 0
         * @ensures this.atoms' = atoms
         * @throws NullPointerException atoms = null
         * @throws IllegalArgumentException some a: atoms[int] | a !in
         *             universe.atoms[int]
         */
        IntTuple(final Object... atoms) {
            this.arity = atoms.length;
            checkCapacity(arity);
            int tempIndex = 0, multiplier = 1;
            for (int i = arity - 1; i >= 0; i--) {
                tempIndex += universe.index(atoms[i]) * multiplier;
                multiplier *= base;
            }
            this.index = tempIndex;
            assert this.index >= 0;
        }

        /**
         * Constructs a tuple with the specified arity, with the specified atom at each
         * position.
         *
         * @ensures this.arity' = arity && this.atoms = [0..arity)->atom
         * @throws NullPointerException atom = null
         * @throws IllegalArgumentException arity < 1 || atom !in
         *             this.universe.atoms[int]
         */
        @SuppressWarnings("unused" )
        IntTuple(final int arity, final Object atom) {
            checkCapacity(arity);
            if (arity < 1)
                throw new IllegalArgumentException("arity < 1");
            this.arity = arity;
            int tempIndex = 1;
            for (int i = 0; i < arity; i++) {
                tempIndex = tempIndex * base + 1;
            }
            this.index = universe.index(atom) * tempIndex;
            assert this.index >= 0;
        }

        /** {@inheritDoc} */
        @Override
        public Universe universe() {
            return universe;
        }

        /** {@inheritDoc} */
        @Override
        public int arity() {
            return arity;
        }

        /** {@inheritDoc} */
        @Override
        public int index() {
            return index;
        }

        /** {@inheritDoc} */
        @Override
        public Object atom(int i) {
            return universe.atom(atomIndex(i));
        }

        /** {@inheritDoc} */
        @Override
        public int atomIndex(int i) {
            return project(index, arity, i);
            // if (i < 0 || i >= arity) throw new IndexOutOfBoundsException("i <
            // 0 || i >= this.arity");
            // return (index / ((int) Math.pow(base, arity-1-i))) % base;
        }

        /** {@inheritDoc} */
        @Override
        public boolean contains(Object atom) {
            for (int remainder = index, atomIndex = universe.index(atom); remainder > 0; remainder = remainder / base) {
                if (remainder % base == atomIndex)
                    return true;
            }
            return false;
        }

        /** {@inheritDoc} */
        @Override
        public Tuple product(Tuple tuple) {
            if (!universe.equals(tuple.universe()))
                throw new IllegalArgumentException("tuple.universe != this.universe");
            return new IntTuple(arity + tuple.arity(), index * ((int) Math.pow(base, tuple.arity())) + tuple.index());
        }
    }

}
